The following content has been provided by the University of Erlangen-Nürnberg.

While the beamer is still heating up, we do have a day for the exam.

You may have seen it is February 11th and we will hopefully know the time on Monday.

The problem is that we are a big course and we need a lot of space for doing an exam,

which seems to be difficult to come by.

So, hopefully Monday.

If there are any collisions with other exams, talk to me.

We can always do things like let you write the time slot before or after

and then kind of see that you can't tell the others of what you've seen.

That works. So you don't have to wait a semester.

We also, I don't know whether anybody is, probably not.

We also have a date for the AI2 retake exam.

Probably most of you aren't interested.

Nothing.

A pen, your mascot.

Yeah.

Something to eat.

I don't want anybody falling over because they don't have enough blood sugar, but anything else, no.

And of course, anything that's covered in the course before the exam can be on the exam.

Any more questions about the exam?

We will print a lot of paper with a lot of space for you, and you can write onto that paper.

You don't have to bring your own paper.

Good.

Yesterday, we wrapped up First Order Logic.

And in particular, we talked about machine-oriented calcali for theorem proving in First Order Logic,

proving new knowledge from old knowledge, knowledge that is entailed by the current world state in an expressive logic.

And since we have an expressive logic, we should not be shocked that the inference procedures are getting a little bit more difficult.

In this particular case, we looked at two inference procedures.

One is First Order Tableaus, where the central innovation is that instead of closing complementary literals,

namely a false and a true together must be a contradiction, we relax that by saying,

do we find in the tableau two literals that we can make contradictory via a substitution?

That shifts some of the problem, namely the problem of choosing the right terms in the universal rule,

up to a later place where we hopefully have more information.

And by and large, in practice, this works very well, as we've seen in the example.

So the problem is that we want to solve, is can we find a substitution that makes two terms in First Order Logic equal?

And can we do so with the least amount commitment possible?

And it turns out that there's an algorithm for that called unification.

The algorithm is one that lends itself to being written down as a calculus.

And if that is the case, we can use the calculus to make certain kinds of properties of the algorithm,

make them explicit and prove things about them.

So what you've seen yesterday in a sequence of Lemata was we actually proved properties of this algorithm,

something we haven't done before.

Normally, I show you a little bit of pseudocode, wave my hands vigorously and say,

oh yeah, obviously it does what we want.

And then you probably think a bit and say, yeah, it probably does what we want.

And normally we would go about, if we had an algorithm like that, implement it, test it and see whether it does the expected thing.

Does it find Rome when you're looking for a wayfinding or does it end up in Bucharest or something like that?

If it ends up in Bucharest when you want to go to Rome, you say,

oh, that's probably an error if we have to do something to the algorithm.

Here we've done something different.